$\forall$$T$:Type, $L$:($T$ List).
\\[0ex](0 $<$ $\parallel$$L$$\parallel$) $\Rightarrow$ ($\forall$$x$:$T$. ($x$ $\in$ $L$) $\Rightarrow$ ($\neg$($x$ = hd($L$))) $\Rightarrow$ hd($L$) before $x$ $\in$ $L$)